msg{-}spec1($k$; $l$; ${\it tg}$; $n$; $s$,$v$.$f$($s$;$v$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}single($<$$k$, $l$$>$; cons($<$${\it tg}$, $n$, $\lambda$$s$,$v$. cons($f$($s$;$v$); [])$>$; []))